Superposition for Fixed Domains
Identifieur interne : 004301 ( Main/Exploration ); précédent : 004300; suivant : 004302Superposition for Fixed Domains
Auteurs : Matthias Horbach [Allemagne] ; Christoph Weidenbach [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a perfect term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the perfect model’s term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and complete for a first-order fixed domain semantics. For some classes of formulas and theories, we can even employ the calculus to prove properties of the perfect model itself, going beyond the scope of known superposition based approaches.
Url:
DOI: 10.1007/978-3-540-87531-4_22
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003037
- to stream Istex, to step Curation: 002F98
- to stream Istex, to step Checkpoint: 000D29
- to stream Main, to step Merge: 004412
- to stream Main, to step Curation: 004301
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Superposition for Fixed Domains</title><author><name sortKey="Horbach, Matthias" sort="Horbach, Matthias" uniqKey="Horbach M" first="Matthias" last="Horbach">Matthias Horbach</name></author><author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:CBC99CC5C3F6C38AAE7957A16F55BA5FD00D7504</idno><date when="2008" year="2008">2008</date><idno type="doi">10.1007/978-3-540-87531-4_22</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-NZKFH25Z-G/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003037</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003037</idno><idno type="wicri:Area/Istex/Curation">002F98</idno><idno type="wicri:Area/Istex/Checkpoint">000D29</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000D29</idno><idno type="wicri:doubleKey">0302-9743:2008:Horbach M:superposition:for:fixed</idno><idno type="wicri:Area/Main/Merge">004412</idno><idno type="wicri:Area/Main/Curation">004301</idno><idno type="wicri:Area/Main/Exploration">004301</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Superposition for Fixed Domains</title><author><name sortKey="Horbach, Matthias" sort="Horbach, Matthias" uniqKey="Horbach M" first="Matthias" last="Horbach">Matthias Horbach</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max-Planck-Institut für Informatik, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max-Planck-Institut für Informatik, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a perfect term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the perfect model’s term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and complete for a first-order fixed domain semantics. For some classes of formulas and theories, we can even employ the calculus to prove properties of the perfect model itself, going beyond the scope of known superposition based approaches.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Sarre (Land)</li></region><settlement><li>Sarrebruck</li></settlement></list><tree><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Horbach, Matthias" sort="Horbach, Matthias" uniqKey="Horbach M" first="Matthias" last="Horbach">Matthias Horbach</name></region><name sortKey="Horbach, Matthias" sort="Horbach, Matthias" uniqKey="Horbach M" first="Matthias" last="Horbach">Matthias Horbach</name><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004301 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004301 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:CBC99CC5C3F6C38AAE7957A16F55BA5FD00D7504
|texte= Superposition for Fixed Domains
}}
| This area was generated with Dilib version V0.6.33. |  |